/*
 * LPB.hpp
 *
 * Copyright 2012 Fabian Wenzelmann, Christian Schilling
 *
 * This file is part of Recognition-Procedures-for-Boolean-Functions.
 *
 * Recognition-Procedures-for-Boolean-Functions is free software: you
 * can redistribute it and/or modify it under the terms of the
 * GNU General Public License as published by the Free Software Foundation,
 * either version 3 of the License, or (at your option) any later version.
 *
 * Recognition-Procedures-for-Boolean-Functions is distributed in the hope
 * that it will be useful, but WITHOUT ANY WARRANTY; without even the implied
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General
 * Public License for more details.
 *
 * You should have received a copy of the GNU General Public License
 * along with Recognition-Procedures-for-Boolean-Functions.
 *
 * If not, see <http://www.gnu.org/licenses/>.
 */

#ifndef LPB_HPP_
#define LPB_HPP_

#include <functional>
#include <string>
#include <vector>
#include <iostream>

#include "bfr/Literal.hpp"
#include "bfr/CoefficientType.hpp"
#include "bfr/ClauseSet.hpp"

namespace bfr {

/**
 * A summand of the LPB.
 *
 * Such a summand is just one of the \f$a_il_i\f$ expressions.
 */
class LPBSummand {
    public:
    /**
     * Constructor.
     *
     * @param c The coefficient of the summand, that is the
     * \f$a_i\f$ of the summand.
     * @param l The literal of the summand, that is the \f$l_i\f$.
     */
    LPBSummand(lpb_coefficient_t c, const Literal &l)
    : coeff(c), literal(l) { };

    /**
     * Copy constructor.
     */
    LPBSummand(const LPBSummand &other)
    : coeff(other.coeff), literal((other.literal)) { }

    // default constructor
    LPBSummand() : coeff(-1), literal(0) { };

    /**
     * Destructor.
     */
    ~LPBSummand() { };

    LPBSummand& operator= (const LPBSummand &other) {
        coeff = other.coeff;
        literal = other.literal;
        return *this;
    }

    /**
     * Return the coefficient.
     *
     * @return The coefficient \f$a_i\f$.
     */
    lpb_coefficient_t getCoefficient() const { return coeff; };

    /**
     * Return the Literal.
     *
     * @return The literal \f$l_i\f$.
     */
    const Literal &getLiteral() const { return literal; };

    /**
     * Compare two LPBSummands.
     *
     * Two summand are equal if they have the same
     * coefficient and the same Literal.
     */
    bool operator ==(const LPBSummand& other) {
        return (coeff == other.coeff) && (literal == other.literal);
    }

    /**
     * Write operator to a stream.
     *
     * @return The stream <code>out</code>.
     */
    friend std::ostream& operator<<(std::ostream &out,
            const LPBSummand &s) {
        out << s.coeff;
        out << ' ';
        const Literal &l = s.literal;
        if (l.getPolarity()) {
            l.variableString(out);
        }
        else {
            out << "(1 - ";
            l.variableString(out);
            out << ')';
        }
        return out;
    }

    /**
     * Compares two LPSummands.
     *
     * A Summand is said to be greater than another summand
     * if its coefficient is greater. If the coefficients are equal
     * it depends on the ids of the literals, i. e. a Literal
     * with greater index is greater.
     *
     * The polarity is not taken into account.
     */
    struct CompareEntriesG
            : public std::binary_function<const LPBSummand&,
              const LPBSummand&,
              bool>
    {
        public:
            bool operator() (const LPBSummand &first,
                    const LPBSummand &second) const {
                const lpb_coefficient_t firstCoeff =
                        first.getCoefficient();
                const lpb_coefficient_t secondCoeff =
                        second.getCoefficient();
                if (firstCoeff > secondCoeff) {
                    return true;
                }
                else if (firstCoeff < secondCoeff) {
                    return false;
                }
                else {
                    const size_t firstID =
                            first.getLiteral().getId();
                    const size_t secondID =
                            second.getLiteral().getId();
                    return firstID > secondID;
                }
            }
    };

            private:
    // coefficient
    lpb_coefficient_t coeff;
    // literal
    Literal literal;

};

/**
 * A class representing LPBs.
 *
 * An LPB is an expression of the form \f$a_1l_1 + \dots + a_ml_m \geq d\f$
 * where \f$a_i, d\f$ are natural numbers, \f$l_i\f$ are literals.
 *
 * For more information about LPBs you may see some of the papers
 * <ul>
 * <li>
 * <a href="http://www.informatik.uni-freiburg.de/~ki/papers/smaus-tr230.pdf">
 * Smaus 2007
 * </a>
 * </li>
 * </ul>
 */
class LPB {
    public:
        /**
         * Constructor.
         *
         * Construct a new LPB given the degree and an initial capacity.
         *
         * @param degree The degree \f$d\f$ of the degree.
         * @param initialCapacity The initial capacity of the vector.
         */
        explicit
        LPB(const lpb_coefficient_t degree, const size_t initialCapacity=8);

        /**
         * Copy constructor.
         */
        explicit LPB(const LPB& other);

        /**
         * Destructor.
         */
        ~LPB();

        /**
         * Write LPB to stream.
         *
         * @return The stream <code>out</code>.
         */
        friend std::ostream& operator<<(std::ostream &out,
                const LPB &l);

        /**
         * Return a string representation of this LPB.
         *
         * @return Human readable string representation.
         */
        std::string asString() const;

        /**
         * Add a new summand to the LPB.
         *
         * @param coefficient The coefficient of the summand.
         * @param literal The Literal of the summand.
         */
        void addSummand(lpb_coefficient_t coefficient,
                const Literal &literal);

        /**
         * Return the LPBSummand at the specified position.
         *
         * If the input is <code>i</code> this method returns
         * the LPBSummand \f$a_il_i\f$.
         *
         * @param index The index of the summand.
         *
         * @return \f$a_il_i\f$.
         */
        const LPBSummand& operator[](size_t index) const;

        /**
         * Return the degree \f$d\f$ of the LBP.
         *
         * @return \f$d\f$.
         */
        lpb_coefficient_t getDegree() const;

        /**
         * Return the number of summands in the LPB.
         *
         * If the LPB is \f$a_1l_1 + \dots + a_ml_m \geq d\f$ this
         * method returns \f$m\f$.
         *
         * @return The number of summands in the LPB.
         */
        size_t size() const;

        /**
         * Sort the coefficients.
         *
         * This will sort the coefficients according the order defined
         * in LPB::LPBSummand::CompareEntriesG.
         */
        void sortCoefficients();

        /**
         * Convert the LPB to a DNF that is equivalent to the LPB.
         */
        ClauseSet *toDNF() const;

    private:
        // the degree
        lpb_coefficient_t degree;
        // the summands
        std::vector<LPBSummand> summands;
};

}

#endif  // LPB_HPP_
